da:k:Knd fp Type. Msg(da)  Type 

latex

Definitions	Msg(da), Msg(M), f(x)?z, KindDeq, rcv(l,tg), Id, IdLnk, a:A fp B(a), x:A. B(x), x. t(x), t  T, Knd
Lemmas	Knd wf, fpf wf, IdLnk wf, Id wf, rcv wf, Kind-deq wf, fpf-cap wf, Msg wf